Inference at * 1 2 3 
Iof proof for Lemma sub-equality:

.....wf..... NILNIL

1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
7. P(i)
8. T
  {j:T| P(j)}  = {j:T| P(j)}  

latex

 by Auto 

latex

 .

Definitions

Type, , f(a), {x:A| B(x)}